package test;

import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import sign.FormulaSign;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;

public class Ttest {
    public static void test(){
        UnaryFormula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        UnaryFormula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));
        UnaryFormula c=new UnaryFormula(new UnaryLiteral(new UnaryAtom("c"),false));
        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,a,b);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.ANY,b,c);

        ArrayList<Formula> formulas=new ArrayList<>();
        formulas.add(bf1);
        formulas.add(bf2);
        Set<Formula> tset=new HashSet<>();

        for (Formula f : formulas) {
            BinaryFormula bf=(BinaryFormula) f;//此时的输入应该都为bf，可以进行类型转换
            tset.add(bf.getLeft());
            tset.add(bf.getRight());
        }

        for (Formula formula:tset) {//对tSet中的元素依次应用TRules
            //System.out.println(formula);
            BinaryFormula result=new BinaryFormula(FormulaSign.ANY,formula,formula);
            System.out.println(result);
        }
    }

    public static void main(String[] args) {
        test();
    }

}
